perm filename XXX[1,JRA]5 blob
sn#092454 filedate 1974-03-19 generic text, type T, neo UTF8
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 1,1
******** PROVE1.NEW **** PAGE 1
1) 01600 MKWRD
*** PROVE2.NEW *** PAGE 1
2) ISCLS
2) ISCL
2) ISLIT
2) ISTRM
2) MKWRD
******** PROVE1.NEW **** PAGE 1
1) 05450 DEP DEP1
1) 05500 DEL
1) 05800 DOWN
*** PROVE2.NEW *** PAGE 1
2) DEL
2) DOML
2) DOMC
2) DOWN
******** PROVE1.NEW **** PAGE 1
1) 08500 MAX
*** PROVE2.NEW *** PAGE 1
2) MATCHER
2) MATCH1
2) MATCHTR
2) MATCHPN
2) MATMLT
2) MATMLT*
2) MAX
******** PROVE1.NEW **** PAGE 1
1) 09900 ONEGSGN
*** PROVE2.NEW *** PAGE 1
2) NOSYM
2) OCR
2) OCR1
2) ONEGSGN
******** PROVE1.NEW **** PAGE 1
1) 12300 SET1
*** PROVE2.NEW *** PAGE 1
2) RESET
2) RESET1
2) SET1
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 1,1
******** PROVE1.NEW **** PAGE 1
1) 14200 SUBST1
*** PROVE2.NEW *** PAGE 1
2) SUBSUME*
2) SUBST1
******** PROVE1.NEW **** PAGE 1
1) 15000 TRY
*** PROVE2.NEW *** PAGE 1
2) TREE
2) TREEDEP
2) TRY
******** PROVE1.NEW **** PAGE 1
1) 16600 UPDATESTATE
*** PROVE2.NEW *** PAGE 1
2) UPGETNU
2) UPDATESTATE
******** PROVE1.NEW **** PAGE 1
1) 17200 VINE
*** PROVE2.NEW *** PAGE 1
2) VARIT
2) VINE
******** PROVE1.NEW **** PAGE 1
1) 22000 (DEFPROP MKWRD
*** PROVE2.NEW *** PAGE 1
2) (DEFPROP ISCLS
2) (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 1))
2) MACRO)
2) (DEFPROP ISCL
2) (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 2))
2) MACRO)
2) (DEFPROP ISLIT
2) (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 3))
2) MACRO)
2) (DEFPROP ISTRM
2) (LAMBDA (L) (LIST (QUOTE EQ) (CADR L) 4))
2) MACRO)
2) (DEFPROP MKWRD
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 1,1
******** PROVE1.NEW **** PAGE 1
1) 36000 (LAMBDA(X1)
1) 36100 (PROG ( N DLIST Z2 D M SAVEED SAVESTR)
1) 36400 (SETQ N 1)
1) 36500 (SETQ M (SETQ D 0))
*** PROVE2.NEW *** PAGE 1
2) (LAMBDA(XX)
2) (PROG (X1 Z2 D M STRATEGY SUPPORT EDITSTRAT MERGE ORDER DEBUG ANCESTRY PMODEL NMODEL PFLG PDEPTH DLIST)
2) (COND (EQUAL (SETQ PFLG NIL)) (T (SETQ PFLG NIL)))
2) (SETQ PDEPTH 3)
2) (SETQ DDEPTH 4)
2) (SETQ X1 XX)
2) (SETQ M (SETQ D 0))
******** PROVE1.NEW **** PAGE 1
1) 37100 (SETQ DLIST(CONS N DLIST))))
1) 37200 (SETQ X1 (CDR X1))
1) 37250 (COND((NULL X1)(GO B)))
1) 37300 (COND ((CDR X1)(SETQ N(ADD1 N)) (GO A)))
1) 37500 (SETQ M (DIFFERENCE (PLUS M (LENGTH (CDAR X1))) 2))
1) 37600 B (COND ((NOT (GREATERP M 0)) (SETQ M 1)))
1) 37650 (SETQ Z2(ASSOC THEOREMNAME NEWNAME))
1) 37700 (SETQ D(ADD1 D))
1) 37750 (COND(STRAT(COND((ZEROP ITER)(SETQ ITER 1)(COND((NOT(EQ M 1))(SETQ M(ADD1 M)))(T(SETQ D(ADD1 D)
1) 37775 ))))(T(SETQ D(ADD1 D))(SETQ ITER 0)))))
1) 37800 (COND(Z2
1) 38000 (SETQ SAVESTR (LIST @AND @ANCESTRY (LIST @SUPPORT THEOREMNAME))))
1) 38100 (T (SETQ SAVESTR (QUOTE ANCESTRY))))
1) 38200 (SETQ SAVEED
1) 38300 (LIST @OR (LIST @MAXDEPTH @(CDR C) D)
1) 38400 (LIST @MAXLENGTH @C M)))
1) 38500 (COND((AND EQUAL DLIST)(SETQ SAVEED(LIST @AND (LIST @DEMOD DLIST 4) SAVEED))))
1) 38600 (SETQ DEBUG T)
1) 38700 (COND
1) 38800 (EQUAL (SETQ SAVESTR (CONS (QUOTE AND) (CONS SAVESTR (LIST (LIST (QUOTE EQUALITY) EQUAL 3)))))))
1) 38900 (RETURN
1) 39000 (CONS SAVESTR SAVEED))
1) 39100 ))
1) 39200 EXPR)
*** PROVE2.NEW *** PAGE 1
2) (SETQ DLIST (CONS (CONS (CONS (CAAAR Z2) (CDAR Z2)) (CDR Z2)) DLIST))))
2) (SETQ X1 (CDR X1))
2) (COND ((CDR X1) (GO A)))
2) (SETQ Z2 (ASSOC THEOREMNAME NEWNAME))
2) (COND ((NULL Z2) (GO C)) (T (SETQ Z2 (CDR Z2))))
2) B (COND (Z2 (SETQ SUPPORT (CONS (CDAR Z2) SUPPORT)) (SETQ Z2 (CDR Z2)) (GO B)))
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 1,1
2) C (COND ((NULL LENGTH) (SETQ LENGTH (DIFFERENCE (PLUS M (LENGTH (CDAR X1))) 2)))
2) ((ZEROP ITER) (SETQ LENGTH (ADD1 LENGTH))))
2) (COND ((NOT (GREATERP LENGTH 0)) (SETQ LENGTH 1)))
2) (COND ((NULL DEPTH) (SETQ DEPTH (ADD1 D))) ((NOT (ZEROP ITER)) (SETQ DEPTH (ADD1 DEPTH))))
2) (COND ((ZEROP ITER) (SETQ ITER 1)) (T (SETQ ITER 0)))
2) (COND (SUPPORT (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (OR (SUPPORT C2) (SUPPORT C1)))))
2) (SETQ SAVESTR (QUOTE (AND ANCESTRY (SUPPORT THEOREM)))))
2) (T (SETQ SAVESTR (QUOTE ANCESTRY))))
2) (SETQ ANCESTRY T)
2) (SETQ EDITSTRAT
2) (LIST @LAMBDA @(C)(LIST @OR (LIST @MAXDEPTH @(CDR C) DEPTH)
2) (LIST @MAXLENGTH @C LENGTH))))
2) (SETQ SAVEED(CAR(LAST EDITSTRAT)))
2) (SETQ DEBUG T)
2) (COND (DLIST (SET3 DLIST)))
2) (COND
2) (EQUAL (SETQ SAVESTR (CONS (QUOTE AND) (CONS SAVESTR (LIST (LIST (QUOTE EQUALITY) EQUAL PDEPTH)))))))
2) (RETURN
2) (LIST STRATEGY
2) SUPPORT
2) EDITSTRAT
2) MERGE
2) ORDER
2) DEBUG
2) DEPTH
2) LENGTH
2) ANCESTRY
2) PMODEL
2) NMODEL
2) PFLG
2) EQUAL
2) PDEPTH
2) DLIST))))
2) EXPR)
******** PROVE1.NEW **** PAGE 1
1) 39900 (LAMBDA(Z R)
1) 40000 (PROG ( U1 U4)
1) 40200 ED4 (COND ((NOT Z) (RETURN NIL)) ((OR (NOT (HERE (CAR Z))) (ATOM (CDR (ANCESTOR (CAR Z))))) (GO ED6A)))
*** PROVE2.NEW *** PAGE 1
2) (LAMBDA(L R)
2) (PROG (Z U1 U4)
2) (SETQ Z L)
2) ED4 (COND ((NOT Z) (RETURN NIL)) ((OR (NOT (HERE (CAR Z))) (ATOM (CDR (ANCESTOR (CAR Z))))) (GO ED6A)))
******** PROVE1.NEW **** PAGE 1
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 1,1
1) 40500 ED1 (COND ((SUBSUME (CAR U1) U4)(DEL U4) (GO ED4)))
1) 40600 ED6 (SETQ U1 (CDR U1))
*** PROVE2.NEW *** PAGE 1
2) ED1 (COND ((SUBSUME (CAR U1) U4) (GO ED2)))
2) ED6 (SETQ U1 (CDR U1))
******** PROVE1.NEW **** PAGE 1
1) 41100 ))
1) 41200 EXPR)
*** PROVE2.NEW *** PAGE 1
2) ED2 (DEL U4)
2) (GO ED4)))
2) EXPR)
******** PROVE1.NEW **** PAGE 1
1) 43200 (COND ((EQ (CAR X) (QUOTE DEMOD)) (SETQ DDEPTH (CADDR X)) (SETQ DLIST (*CL (CADR X)CLAUSES)) NIL)
1) 43300 (T (CONS (CAR X) (BUILTED1 (CDR X))))))
1) 43400 ((EQ (CAAR X) (QUOTE DEMOD)) (SETQ DDEPTH (CADDAR X)) (SETQ DLIST (*CL (CADAR X)CLAUSES)) (BUILTED1 (CDR X)))
1) 43500 (T (CONS (BUILTED1 (CAR X)) (BUILTED1 (CDR X))))))
*** PROVE2.NEW *** PAGE 1
2) (COND ((EQ (CAR X) (QUOTE DEMOD)) (SETQ DDEPTH (CADDR X)) (SETQ DLIST (*CL (CADR X))) NIL)
2) (T (CONS (CAR X) (BUILTED1 (CDR X))))))
2) ((EQ (CAAR X) (QUOTE DEMOD)) (SETQ DDEPTH (CADDAR X)) (SETQ DLIST (*CL (CADAR X))) (BUILTED1 (CDR X)))
2) (T (CONS (BUILTED1 (CAR X)) (BUILTED1 (CDR X))))))
******** PROVE1.NEW **** PAGE 1
1) 44050 (SETQ PFLG T)(SETQ ANCESTRY NIL)
1) 44100 (SETQ Z (BUILTCH1 X))
*** PROVE2.NEW *** PAGE 1
2) (SETQ Z (BUILTCH1 X))
******** PROVE1.NEW **** PAGE 1
1) 45500 ((EQ (CAR X) (QUOTE SUPPORT)) (SETSUP (CDR X)) (QUOTE(OR (SUPPORT C2)(SUPPORT C1))))
1) 45600 ((EQ (CAR X) (QUOTE MODEL)) (SETQ PMODEL (CADR X))
*** PROVE2.NEW *** PAGE 1
2) ((EQ (CAR X) (QUOTE SUPPORT)) (SETSUP (CDR X)) (QUOTE (SUPPORT C2)))
2) ((EQ (CAR X) (QUOTE MODEL)) (SETQ PMODEL (CADR X))
******** PROVE1.NEW **** PAGE 1
1) 59300 (LAMBDA (C X) (UPGETL1 C X (CONS (CONS (QUOTE CLAUSES) X) NEWNAME)))
1) 59400 EXPR)
*** PROVE2.NEW *** PAGE 1
2) (LAMBDA (C) (UPGETL1 C XYZ1 (CONS (CONS (QUOTE CLAUSES) XYZ1) NEWNAME)))
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 1,1
2) EXPR)
******** PROVE1.NEW **** PAGE 1
1) 65100 (DEFPROP DOWN
*** PROVE2.NEW *** PAGE 1
2) (DEFPROP DOML
2) (LAMBDA NIL (TERMS1 (COND ((NEG (CAR L)) (CDDAR L)) (T (CDAR L))) 100))
2) EXPR)
2) (DEFPROP DOMC
2) (LAMBDA NIL (CDR C))
2) EXPR)
2) (DEFPROP DOWN
******** PROVE1.NEW **** PAGE 1
1) 76000 (LAMBDA (E NAMELIST)
1) 76100 (PROG (Z )
1) 76200 (SCANSET)
*** PROVE2.NEW *** PAGE 1
2) (LAMBDA NIL
2) (PROG (Z Z1)
2) (SCANSET)
******** PROVE1.NEW **** PAGE 1
1) 79150 (AD . USA1)(CO . UTE1)
1) 79200 (DS . UDS1)
*** PROVE2.NEW *** PAGE 1
2) (DS . UDS1)
******** PROVE1.NEW **** PAGE 1
1) 90900 (CDR(ASSOC X VARTBL)))EXPR)
1) 91600 (DEFPROP MAKOVAR
1) 91700 (LAMBDA(X)
1) 91800 (PROG (X1 *NOPOINT Z Z1 M)
1) 91900 (SETQ *NOPOINT T)
1) 92200 (SETQ X1 X)
1) 92300 D(SETQ OUTVAR(NCONC OUTVAR(LIST(CONS VARNO(CAR X1)))))
1) 92350 (SETQ VARTBL(NCONC VARTBL(LIST(CONS (CAR X1)VARNO))))
1) 92400 (SETQ X1 (CDR X1))
1) 92500 (SETQ VARNO(ADD1 VARNO))
1) 92600 (COND (X1 (GO D)))
*** PROVE2.NEW *** PAGE 1
2) (PROG (Z)
2) (SETQ Z (ASSOC X VARTBL))
2) (COND (Z (RETURN (CDR Z))))
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 1,1
2) (SETQ VARTBL (CONS (CONS X (SETQ VARNO (ADD1 VARNO))) VARTBL))
2) (RETURN VARNO)))
2) EXPR)
2) (DEFPROP MAKOVAR
2) (LAMBDA(X)
2) (PROG (X1 *NOPOINT Z N M)
2) (SETQ *NOPOINT T)
2) (SETQ OUTVAR NIL)
2) (SETQ N 1)
2) (SETQ X1 X)
2) D (SETQ OUTVAR (CONS (CONS N (CAR X1)) OUTVAR))
2) (SETQ X1 (CDR X1))
2) (SETQ N (ADD1 N))
2) (COND (X1 (GO D)))
******** PROVE1.NEW **** PAGE 1
1) 92950 C(SETQ Z1(READLIST(APPEND Z(LIST M))))
1) 92975 (SETQ IVAR(CONS Z1 IVAR))
1) 93000 (SETQ OUTVAR(NCONC OUTVAR(LIST(CONS VARNO Z1))) )
1) 93050 (SETQ VARTBL(NCONC VARTBL(LIST(CONS Z1 VARNO))))
1) 93100 (COND ((LESSP M 11) (SETQ VARNO(ADD1 VARNO)) (SETQ M (ADD1 M)) (GO C)))
1) 93200 A (SETQ X (CDR X))
1) 93300 (COND (X (SETQ VARNO (ADD1 VARNO)) (GO B)))
1) 93500 (RETURN OUTVAR)))
*** PROVE2.NEW *** PAGE 1
2) C (SETQ OUTVAR (CONS (CONS N (READLIST (APPEND Z (LIST M)))) OUTVAR))
2) (COND ((LESSP M 11) (SETQ N (ADD1 N)) (SETQ M (ADD1 M)) (GO C)))
2) A (SETQ X (CDR X))
2) (COND (X (SETQ N (ADD1 N)) (GO B)))
2) (SETQ OUTVAR (REVERSE OUTVAR))
2) (RETURN OUTVAR)))
******** PROVE1.NEW **** PAGE 1
1) 05900 (DEFPROP MAX
*** PROVE2.NEW *** PAGE 1
2) (DEFPROP MATCHER
2) (LAMBDA(L)
2) (PROG (FLG Z Z1)
2) (SETQ Z (EVAL (CADR L)))
2) (SETQ Z1 (CAR L))
2) (COND ((ATOM (CADR L))
2) (COND ((MEMQ (CADR L) (QUOTE (T1 T2 T3 T4))) (SETQ FLG 4))
2) ((MEMQ (CADR L) (QUOTE (L1 L2 L3 L4))) (SETQ FLG 3))
2) ((MEMQ (CADR L) (QUOTE (C))) (SETQ FLG 2) (SETQ Z (CDR Z)))
2) (T (ERR NIL))))
2) ((EQ (CAADR L) (QUOTE TREE)) (SETQ FLG 1))
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 1,1
2) (T (ERR NIL)))
2) (COND ((ATOM Z1) (RETURN (MATCH1 Z1 Z FLG)))
2) ((EQ (CAR Z1) (QUOTE AND)) (GO MAA1))
2) ((EQ (CAR Z1) (QUOTE OR)) (GO MAO1))
2) (T (RETURN (MATCH1 Z1 Z FLG))))
2) MAA1 (SETQ Z1 (CDR Z1))
2) MAAND
2) (COND ((NULL Z1) (RETURN T)) ((MATCH1 (CAR Z1) Z FLG) (GO MAA1)) (T (RETURN NIL)))
2) MAO1 (SETQ Z1 (CDR Z1))
2) MAOR (COND ((NULL Z1) (RETURN NIL)) ((MATCH1 (CAR Z1) Z FLG) (RETURN T)))
2) (GO MAO1)))
2) FEXPR)
2) (DEFPROP MATCH1
2) (LAMBDA(X Y FL)
2) (COND ((ATOM X)
2) (COND ((EQ X (QUOTE %NG)) (COND ((ISLIT FL) (NEG Y)) ((ISCL FL) (MATCHPN Y T)) (T (ERR NIL))))
2) ((EQ X (QUOTE %PL)) (COND ((ISLIT FL) (NOT (NEG Y))) ((ISCL FL) (MATCHPN Y NIL)) (T (ERR NIL))))
2) ((NUMBERP X) (COND ((ISCLS FL) (MATCHTR X Y)) (T (MATMLT X Y FL))))
2) ((AND (MEMQ X (QUOTE (C1 C2))) (ISCLS FL)) (MEMQ (EVAL X) Y))
2) (T (ERR NIL))))
2) ((NUMBERP (CAR X)) (COND ((ISCLS FL) (MATCHTR (CAR X) Y)) (T (MATMLT (CAR X) Y FL))))
2) ((EQ (LENGTH X) 1) (MATMLT (CAR X) Y FL))
2) ((ISCLS FL) (COND ((EQ (CAR X) (QUOTE CL)) (MATCHTR (CADR X) Y)) (T NIL)))
2) (T (MATMLT* X Y FL))))
2) EXPR)
2) (DEFPROP MATCHTR
2) (LAMBDA (N TR) (MEMQ (CAR (DOWN N CLAUSES)) TR))
2) EXPR)
2) (DEFPROP MATCHPN
2) (LAMBDA(X FL)
2) (PROG (Z)
2) A (SETQ Z (NEG (CAR X)))
2) (COND ((AND Z FL) (RETURN T)) ((AND (NOT Z) (NOT FL)) (RETURN T)))
2) (SETQ X (CDR X))
2) (COND (X (GO A)))
2) (RETURN NIL)))
2) EXPR)
2) (DEFPROP MATMLT
2) (LAMBDA(X Y FL)
2) (PROG NIL
2) (COND ((AND (ISTRM FL) (NOT (ASSOC X TBL))) (ERR NIL))
2) ((ISTRM FL) (RETURN (OCR X Y)))
2) ((ISLIT FL) (RETURN (COND ((NEG Y) (OCR X (CDR Y))) (T (OCR X Y))))))
2) A (COND ((COND ((NEG (CAR Y)) (OCR X (CDAR Y))) (T (OCR X (CAR Y)))) (RETURN T)))
2) (SETQ Y (CDR Y))
2) (COND (Y (GO A)))
2) (RETURN NIL)))
2) EXPR)
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 1,1
2) (DEFPROP MATMLT*
2) (LAMBDA(X Y FL)
2) (PROG (Z)
2) (COND ((AND (ISTRM FL) (NOT (ASSOC (CAR X) TBL))) (ERR NIL))
2) ((EQ (CAR X) (QUOTE %NG)) (SETQ X (CDR X)) (GO M1))
2) ((NOT (ISCL FL)) (SETQ Y (LIST Y))))
2) D (SETQ X (VARIT (LIST X)))
2) B (SETQ Z (TERMS1 (LIST (COND ((NEG (CAR Y)) (CDAR Y)) (T (CAR Y)))) 64))
2) A (COND ((UNI X (CAR Z) NIL) (RETURN T)))
2) (SETQ Z (CDR Z))
2) (COND (Z (GO A)))
2) (SETQ Y (CDR Y))
2) (COND (Y (GO B)))
2) (RETURN NIL)
2) M1 (COND ((NEG (CAR Y)) (GO M2)))
2) M3 (SETQ Y (CDR Y))
2) (COND (Y (GO M1)))
2) (RETURN NIL)
2) M2 (COND ((EQ (LENGTH X) 1) (COND ((EQ (CADAR Y) (CAR X)) (RETURN T)) (T (GO M3)))) (T (GO D)))))
2) EXPR)
2) (DEFPROP MAX
******** PROVE1.NEW **** PAGE 2
1) 17200 (DEFPROP ONEGSGN
*** PROVE2.NEW *** PAGE 2
2) (DEFPROP NOSYM
2) (LAMBDA (L) (COND ((NULL L) 0) ((ATOM L) 1) (T (MAX (ADD1 (NOSYM (CAR L))) (NOSYM (CDR L))))))
2) EXPR)
2) (DEFPROP OCR
2) (LAMBDA (X Y) (OCR1 X (LIST Y)))
2) EXPR)
2) (DEFPROP OCR1
2) (LAMBDA(X Y)
2) (COND ((NULL Y) NIL)
2) ((VAR (CAR Y)) (OCR1 X (CDR Y)))
2) ((CONST (CAR Y)) (COND ((EQ (CAAR Y) X) T) (T (OCR1 X (CDR Y)))))
2) ((EQ X (CAAR Y)) T)
2) ((OCR1 X (CDAR Y)) T)
2) (T (OCR1 X (CDR Y)))))
2) EXPR)
2) (DEFPROP ONEGSGN
******** PROVE1.NEW **** PAGE 2
1) 44900 (OUTIT(CAR STRAT))
1) 45000 (PRINT (QUOTE EDIT-STRATEGY-IS:))
1) 45100 (OUTIT(CDR STRAT))
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 2,2
1) 45200 (PRINT (QUOTE ELAPSED-TIME))
*** PROVE2.NEW *** PAGE 2
2) (OUTIT SAVESTR)
2) (PRINT (QUOTE EDIT-STRATEGY-IS:))
2) (OUTIT SAVEED)
2) (PRINT (QUOTE ELAPSED-TIME))
******** PROVE1.NEW **** PAGE 2
1) 46650 (DE REENTER()(TRYIT))
1) 46700 (DEFPROP REDUCER
*** PROVE2.NEW *** PAGE 2
2) (DEFPROP REDUCER
******** PROVE1.NEW **** PAGE 2
1) 56000 (DEFPROP SET1
*** PROVE2.NEW *** PAGE 2
2) (DEFPROP RESET
2) (LAMBDA(L)
2) (PROG (Z) R1 (SETQ Z (EVAL (CONS (QUOTE RESET1) (CAR L)))) (SETQ L (CDR L)) (COND (L (GO R1))) (RETURN Z)))
2) FEXPR)
2) (DEFPROP RESET1
2) (LAMBDA(L)
2) (PROG (X Z2 Z3 ZZ XX Z Z1 F1)
2) (SETQ Z STATEVECTOR)
2) A (COND
2) ((EQ (CAR L) (CAR Z)) (SETQ F1 T)
2) (COND ((EQ (CAR L) (QUOTE STRATEGY)) (GO R1))
2) (T (SET (CAR Z) (EVAL (CADR L)))))))
2) R2 (SETQ Z1 (CONS (EVAL (CAR Z)) Z1))
2) (SETQ Z (CDR Z))
2) (COND (Z (GO A)))
2) (COND (F1 (RETURN (REVERSE Z1))))
2) R3 (PRINT (QUOTE UNDEFINED-ARG-FOR-RESET:))
2) (PRINC (CAR L))
2) (TERPRI)
2) (ERR NIL)
2) R1 (SETQ X (QUOTE (X)))
2) (SETQ L (CDR L))
2) R4 (SETQ Z2 (CAR L))
2) (COND ((ATOM Z2) (SETQ Z3 Z2)) (T (SETQ Z3 (CAR Z2))))
2) SPQ2 (COND ((NOT (MEMQ Z3 STRATLIST)) (GO R3))
2) ((EQ Z3 (QUOTE SUPPORT)) (SETQ XX (EVAL (CADAR L)))
2) (PROG (ZZ)
2) (GO B)
2) A (SETQ ZZ (CONS (CDAR XX) ZZ))
2) (SETQ XX (CDR XX))
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 2,2
2) B (COND (XX (GO A)))
2) (SETQ SUPPORT ZZ))
2) (SETQ ZZ (QUOTE (SUPPORT C2))))
2) ((EQ Z3 (QUOTE MODEL)) (SETQ PMODEL (CADAR L))
2) (SETQ NMODEL (CADDAR L))
2) (SETQ ZZ (CONS (CONS Z3 X) ZZ)))
2) ((EQ Z3 (QUOTE ANCESTRY)) (SETQ ANCESTRY T))
2) ((EQ Z3 (QUOTE ORDER)) (SETQ ORDER T))
2) ((EQ Z3 (QUOTE MERGE)) (SETQ MERGE T))
2) (T (SETQ ZZ (CONS (CONS Z3 X) ZZ))))
2) (SETQ L (CDR L))
2) (COND (L (GO R4)))
2) (COND (ZZ (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (SUPPORT C2))))) (T (SETQ STRATEGY NIL)))
2) (GO R2)))
2) FEXPR)
2) (DEFPROP SET1
******** PROVE1.NEW **** PAGE 2
1) 67900 SAVESTR SAVEED)
1) 68000 (SETQ CHAN (OUTC NIL NIL))
1) 68100 (COND(FLG(SETQ SAVEED(CDR STRAT))(SETQ SAVESTR(CAR STRAT))))
1) 68200 (SETQ XYZ1 XX)
*** PROVE2.NEW *** PAGE 2
2) SUPPORT
2) EDITSTRAT
2) MERGE
2) ORDER
2) DEBUG
2) DEPTH
2) LENGTH
2) ANCESTRY
2) STRATEGY
2) PMODEL
2) NMODEL
2) PFLG
2) PDEPTH
2) DLIST)
2) (SETQ CHAN (OUTC NIL NIL))
2) (SETQ PFLG T)
2) (COND (FLG (UPDATESTATE YY)))
2) (SETQ XYZ1 XX)
******** PROVE1.NEW **** PAGE 2
1) 68900 AA (CLAUSES XX)
*** PROVE2.NEW *** PAGE 2
2) (SETQ N 1)
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 2,2
2) AA (CLAUSES XX)
******** PROVE1.NEW **** PAGE 2
1) 69600 (QUOTE "ANCESTRY VINE UNIT MODEL[POS ; NEG] DEFMODEL[NAME] P1
1) 69700 SUPPORT[#,..] EQUALITY[ID,#] "))
*** PROVE2.NEW *** PAGE 2
2) (QUOTE "ANCESTRY VINE UNIT MODEL[POS ; NEG] DEFMODEL[NAME] P1 P2
2) SUPPORT[#,..] EQUALITY[ID,#] "))
******** PROVE1.NEW **** PAGE 2
1) 70900 (SETQ SAVESTR(SETQ ZIN (TOP)))
1) 71000 (OUTIT ZIN)
1) 71100 SRB (SETQ DEBUG T)
*** PROVE2.NEW *** PAGE 2
2) (SETQ ZIN (TOP))
2) (SETQ STRATEGY (BUILTCH ZIN))
2) (OUTIT ZIN)
2) (SETQ SAVESTR ZIN)
2) SRB (SETQ DEBUG T)
******** PROVE1.NEW **** PAGE 2
1) 71400 (FLG (OUTIT SAVEED)
1) 71500 (PRINT (QUOTE DO-YOU-WANT-TO-CHANGE-IT))
*** PROVE2.NEW *** PAGE 2
2) (FLG (OUTIT (CAR (LAST EDITSTRAT)))
2) (PRINT (QUOTE DO-YOU-WANT-TO-CHANGE-IT))
******** PROVE1.NEW **** PAGE 2
1) 72300 (SETQ SAVEED (SETQ ZIN (TOP)))
1) 72400 (OUTIT ZIN)
*** PROVE2.NEW *** PAGE 2
2) (SETQ ZIN (TOP))
2) (SETQ SAVEED ZIN)
2) (SETQ EDITSTRAT (BUILTED ZIN))
2) (OUTIT ZIN)
******** PROVE1.NEW **** PAGE 2
1) 72700 (CONS SAVESTR SAVEED))
1) 72800 (OUTC CHAN NIL)
*** PROVE2.NEW *** PAGE 2
2) (LIST STRATEGY
2) SUPPORT
2) EDITSTRAT
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 2,2
2) MERGE
2) ORDER
2) DEBUG
2) DEPTH
2) LENGTH
2) ANCESTRY
2) PMODEL
2) NMODEL
2) PFLG
2) EQUAL
2) PDEPTH
2) DLIST))
2) (OUTC CHAN NIL)
******** PROVE1.NEW **** PAGE 2
1) 73500 (SETQ X (*CL X CLAUSES))
1) 73600 A (COND ((NULL X) (SETQ SUPPORT Z) (RETURN NIL)))
*** PROVE2.NEW *** PAGE 2
2) (SETQ X (*CL X))
2) A (COND ((NULL X) (SETQ SUPPORT Z) (RETURN NIL)))
******** PROVE1.NEW **** PAGE 2
1) 83800 (DEFPROP SUBST1
*** PROVE2.NEW *** PAGE 2
2) (DEFPROP SUBSUME*
2) (LAMBDA (C D) (PROG NIL (RETURN (SUBSUME1 (CDR C) (POSBIT C) (CDR D) (POSBIT D) NIL))))
2) EXPR)
2) (DEFPROP SUBST1
******** PROVE1.NEW **** PAGE 2
1) 89200 (DEFPROP TRY
*** PROVE2.NEW *** PAGE 2
2) (DEFPROP TREE
2) (LAMBDA(L)
2) (COND ((ATOM (CDR (ANCESTOR L))) (LIST L))
2) (T (NCONC (LIST L) (TREE (CAR (ANCESTOR L))) (TREE (CDR (ANCESTOR L)))))))
2) EXPR)
2) (DEFPROP TREEDEP
2) (LAMBDA(X)
2) (PROG (Z)
2) (SETQ Z (ANCESTOR X))
2) (COND ((ATOM (CDR Z)) (RETURN 0)) (T (RETURN (ADD1 (MAX (TREEDEP (CAR Z)) (TREEDEP (CDR Z)))))))))
2) EXPR)
2) (DEFPROP TRY
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 2,2
******** PROVE1.NEW **** PAGE 2
1) 89800 (PROG (
1) 89850 ITER PREFN EQUAL INFN INFPREDLET IVAR PREPREDLET FNNO FNNAM
1) 89862 VARTBL OUTVAR VARNO
1) 89875 FILENAM PRNO POTZTBL NEWNAME TBL TIME1 Z Z2 AXNO)
1) 89887 (SETQ INFN @(%))(SETQ FNNO 0)(SETQ FNNAM @AXIOM)
1) 89893 (SETQ VARNO 1)
1) 89900 (SETQ ITER(SETQ PRNO 0))
1) 90000 T2 (COND ((NULL L) (SETQ FILENAM (QUOTE (P R F))) (GO P3)))
*** PROVE2.NEW *** PAGE 2
2) (PROG (FILENAM PRNO POTZTBL NEWNAME TBL TIME1 Z Z2 AXNO)
2) (SETQ PRNO 0)
2) T2 (COND ((NULL L) (SETQ FILENAM (QUOTE (P R F))) (GO P3)))
******** PROVE1.NEW **** PAGE 3
1) 08100 (COND ((NULL Z) (GO A1)) ((UNIT C1) (RETURN (LIST NIL))))
*** PROVE2.NEW *** PAGE 3
2) (COND ((NULL Z) (GO A1)))
2) (COND ((NULL Z) (GO A1)) ((UNIT C1) (RETURN (LIST NIL))))
******** PROVE1.NEW **** PAGE 3
1) 27900 (SPECIAL E)
1) 28000 (DEFPROP UPDATE
*** PROVE2.NEW *** PAGE 3
2) (DEFPROP UPDATE
******** PROVE1.NEW **** PAGE 3
1) 29800 Z1R
*** PROVE2.NEW *** PAGE 3
2) UEX
2) Z1R
******** PROVE1.NEW **** PAGE 3
1) 35800 USU1 (SETQ Z1 (ERRSET (GETTERMS E NAMELIST)))
1) 35900 (COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
*** PROVE2.NEW *** PAGE 3
2) USU1 (SETQ Z1 (ERRSET (GETTERMS)))
2) (COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
******** PROVE1.NEW **** PAGE 3
1) 36500 (COND (Z1 (GO USU2)) (T (SETQ NAME (QUOTE ASSERT)) (SETQ Z2(SET3 (SETUP Z3))) (GO UIN1A)))
1) 36600 UUP1 (SETQ Z2 (READ))
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 3,3
*** PROVE2.NEW *** PAGE 3
2) (COND (Z1 (GO USU2)) (T (SETQ NAME (QUOTE ASSERT)) (SETQ Z2 (SETUP Z3)) (GO UIN1A)))
2) UUP1 (SETQ Z2 (READ))
******** PROVE1.NEW **** PAGE 3
1) 43600 UTR1 (SETQ AUTO NIL)
1) 43700 (GO UEX2)
1) 43800 UEX1 (SETQ AUTO T)
1) 43900 UEX2 (SETQ NAME (QUOTE LEMMA))
*** PROVE2.NEW *** PAGE 3
2) UTR1 (SETQ UEX NIL)
2) (GO UEX2)
2) UEX1 (SETQ UEX T)
2) UEX2 (SETQ NAME (QUOTE LEMMA))
******** PROVE1.NEW **** PAGE 3
1) 44200 (SETQ Z2
1) 44300 (ATTEMPT (INITIALAX (CONS THEOREMNAME (APPEND XYZ USING)))
1) 44400 NIL
1) 44500 NIL))
1) 44600 (GO AT1A)
*** PROVE2.NEW *** PAGE 3
2) (SETQ AUTO T)
2) (SETQ Z2
2) (ATTEMPT (INITIALAX (CONS (QUOTE THEOREM) (APPEND XYZ USING)))
2) (COND (UEX (RESET (DLIST (GETNAME (QUOTE DLIST) NAMELIST)) (STRATEGY (SUPPORT XYZ))))
2) (T NIL))
2) NIL))
2) (SETQ AUTO NIL)
2) (GO AT1A)
******** PROVE1.NEW **** PAGE 3
1) 48400 (SETQ AXNO THEOREMNAME)
1) 48500 (SETQ Z3 (COND ((NULL XYZ) (NEGATE (CDAR Z2))) (T (SET3 (SETUP (CNF (LIST (QUOTE NOT) XYZ)))))))
*** PROVE2.NEW *** PAGE 3
2) (SETQ AXNO (QUOTE THEOREM))
2) (SETQ Z3 (COND ((NULL XYZ) (NEGATE (CDAR Z2))) (T (SET3 (SETUP (CNF (LIST (QUOTE NOT) XYZ)))))))
******** PROVE1.NEW **** PAGE 3
1) 55400 (UNSPECIAL E)
1) 55500 (DEFPROP UPGETL
*** PROVE2.NEW *** PAGE 3
2) (DEFPROP UPGETL
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 3,3
******** PROVE1.NEW **** PAGE 3
1) 60600 (SETQ ZZ (APPENDIT ZZ (SET3 (SETUP (CNF(COPY (SETQ XYZ (FIXQFF (CDR Z)))))))))
1) 60700 (GO AS6)
*** PROVE2.NEW *** PAGE 3
2) (SETQ ZZ (APPENDIT ZZ (SET3 (SETUP (CNF (SETQ XYZ (FIXQFF (CDR Z))))))))
2) (GO AS6)
******** PROVE1.NEW **** PAGE 3
1) 62400 (DEFPROP UPDATESTATE
1) 62500 (LAMBDA(L)
1) 62600 (PROG NIL
1) 62700 (SETQ STRATEGY(BUILTCH(CAR L)))
1) 62800 (SETQ EDITSTRAT(BUILTED(CDR L)))
1) 62850 (SETQ STRAT L)
1) 62900 ))
1) 63000 EXPR)
*** PROVE2.NEW *** PAGE 3
2) (DEFPROP UPGETNU
2) (LAMBDA NIL (PROG (Z) (SETQ Z (READ)) (COND ((NUMBERP Z) (READ) (RETURN Z)) (T (RETURN NIL)))))
2) EXPR)
2) (DEFPROP UPDATESTATE
2) (LAMBDA(L)
2) (PROG (L1)
2) (SETQ L1 STATEVECTOR)
2) A (COND ((NULL L) (RETURN NIL)))
2) (SET (CAR L1) (CAR L))
2) (SETQ L (CDR L))
2) (SETQ L1 (CDR L1))
2) (GO A)))
2) EXPR)
******** PROVE1.NEW **** PAGE 3
1) 68100 (DEFPROP VINE
1) 68200 (LAMBDA (X) (ATOM (CDR (ANCESTOR X))))
1) 68300 EXPR)
*** PROVE2.NEW *** PAGE 3
2) (DEFPROP VARIT
2) (LAMBDA(Z)
2) (PROG (Z1 Z2 BL Z3)
2) (SETQ Z3 Z)
2) M1 (SETQ Z2 (CAR Z))
2) (COND ((VAR Z2)
2) (COND ((SETQ Z1 (ASSOC Z2 BL)) (RPLACA Z (CDR Z1)))
2) (T (SETQ BL (CONS (CONS Z2 (SETQ NO (ADD1 NO))) BL)) (RPLACA Z NO))))
2) ((EQ (CAR Z2) (QUOTE _)) (RPLACA Z (SETQ NO (ADD1 NO))))
1) PROVE1.NEW vs. 2) PROVE2.NEW SRCCOM 03-19-74 04:51 PAGES 3,3
2) ((CONST Z2) NIL)
2) (T (VARIT (CDR Z2))))
2) (SETQ Z (CDR Z))
2) (COND (Z (GO M1)))
2) (RETURN Z3)))
2) EXPR)
2) (DEFPROP VINE
2) (LAMBDA (X) (NUMBERP (CDR (ANCESTOR X))))
2) EXPR)
******** PROVE1.NEW **** PAGE 3
1) 70700 (COND (Z (GO D1))) (RETURN NIL)))
1) 70800 EXPR)
*** PROVE2.NEW *** PAGE 3
2) (COND (Z (GO D1)) (RETURN NIL))))
2) EXPR)
******** PROVE1.NEW **** PAGE 3
1) 00300 (DEFPROP DEP
1) 00400 (LAMBDA(L)
1) 00500 (PROG (C1 C2)
1) 00600 (SETQ C1 (CDR C))
1) 00700 A (SETQ C2 (COND ((NEG (CAR C1)) (CDDAR C1)) (T (CDAR C1))))
1) 00800 (COND ((DEP1 C2 (COPY L)) (RETURN T)))
1) 00900 (SETQ C1 (CDR C1))
1) 01000 (COND (C1 (GO A)))
1) 01100 (RETURN NIL)))
1) 01200 FEXPR)
1) 01400 (DEFPROP DEP1
1) 01500 (LAMBDA(C L1)
1) 01600 (PROG (L Z)
1) 01700 A(SETQ L (COPY L1)) (COND ((VAR (CAR C)) (GO B)))
1) 01800 (SETQ Z (ASSOC (CAAR C) L))
1) 01900 (COND ((NULL Z) NIL) ((EQ (CDR Z) 1) (RETURN T)) (T (RPLACD Z (SUB1 (CDR Z)))))
1) 02000 (COND ((NULL (CDAR C)) NIL) ((DEP1 (CDAR C) L) (RETURN T)))
1) 02100 B (SETQ C (CDR C))
1) 02200 (COND (C (GO A)))
1) 02300 (RETURN NIL)))
1) 02400 EXPR)
*** PROVE2.NEW *** PAGE 3